T:Type, l:T List, P:(TProp), a, x:T.
y = succ(x) in a.l
 P(y)
 (x = a  0<||l||  P(hd(l))) & (x = a  y = succ(x) in l P(y)) 

latex

Definitions	t  T, Prop, ||as||, P  Q, False, A, AB, , x:A. B(x), l[i], x(s), P & Q, y = succ(x) in l P(y), hd(l), tl(l), i<j, ij, ij, True, T, P  Q, P  Q
Lemmas	select cons tl, squash wf, le wf, not wf, nat wf, length wf1, select wf